{-
 -  Separ, Type/Satisfiability.hs
 -
 -  Copyright (c) 2010 Dariusz Leniowski. All Rights Reserved.
 -
 -  Redistribution and use in source and binary forms, with or without 
 -  modification, are permitted provided that the following conditions 
 -  are met:
 -
 -  1. Redistributions of source code must retain the above copyright 
 -     notice, this list of conditions and the following disclaimer.
 -
 -  2. Redistributions in binary form must reproduce the above copyright 
 -     notice, this list of conditions and the following disclaimer 
 -     in the documentation and/or other materials provided with 
 -     the distribution.
 -
 -  3. The name of the author may not be used to endorse or promote 
 -     products derived from this software without specific prior 
 -     written permission.
 -
 -  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 
 -  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 
 -  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 
 -  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL 
 -  THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, 
 -  INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES 
 -  (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS 
 -  OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) 
 -  HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, 
 -  STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING 
 -  IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 
 -  POSSIBILITY OF SUCH DAMAGE.
 -
 -}

{-# LANGUAGE FlexibleInstances,FlexibleContexts,UndecidableInstances #-}

-- Module Satisfiability
-- Here be dragons

module Type.Satisfiability where

import Prelude hiding (gcd)

import qualified Data.IntSet as RefSet
import qualified Data.List as List
import Control.Monad

import Type.Base
import Type.ClsType
import Type.ClsData hiding (t)
import Type.Lattice
import Type.Quantifiers()
import Type.Normalize()

---------------------------------------
-- UNIFICATION ALGORIGHM
---------------------------------------

-- consistent [f(..),x,f(..),f(..),y,f(..)] = True
-- consistent [f,f,f,f] = True
-- consistent [f(u1,u2),f(v1,v2),f(w1,w2)] = 
--     consistent [u1,u2] && consistent [v1,v2] && consistent [w1,w2]
-- consistent _ = False

-- common [f(..),x,f(..),y,...] = x
-- common [f,f,f,f] = f
-- common [f(u1,...),f(v1,...),f(w1,...)] = 
--     f(common[u1,v1,w1],...)

-- frontier [f(..),x,f(..),y,...] = {x=f,x=f,x=y,x=f,...}
-- frontier [f,f,f,f] = {}
-- frontier [f(u1,...),f(v1,...),...] = 
--     frontier[u1,v1,...] ++ frontier[u2,v2,...]

{-
while system is not solved do
	select [eq] = [x] containing at least two non-variable terms t_i
	if not consistient(t_i) then abort
	replace terms in [x] by common(t_i)
	for each eq of the form x_i = x_j in frontier(t_i)
		merge two classes [x_i] and [x_j]
	for each equation of the form x_i = t in frontier(t_i)
		add to the class [x_i] term t
end

-}


-- This is O(scary), but seems quick enough in practice.
normaloop :: (Evaluable Type, Normalizable x, Show x) => 
	x -> MM () -> MM x
normaloop x doInside = do
	--shw ("normaloop",x)
	clearBindM
	(x',()) <- normalize x $ uniLoopK $ optimizeBoundsK $ doInside
	getBindM >>= (choice (normaloop x' doInside) (return x'))

instance Evaluable Type => UniLoop a where
	uniLoopK = eqLoopK uniEq uniLeq

-- binds t to r
uniAddTerm :: Evaluable Type => EqId -> RefType -> Type -> MM a -> MM a
uniAddTerm i r t k = do
	uniGetVars t RefSet.empty >>= (mapM_ (uniRebind r) . RefSet.toList)
	setVarValue r t	
	(no,th) <- getVarBounds r
	uniLeq i False no (Ref r) $ uniLeq i False (Ref r) th $ k

uniRebind :: RefType -> RefType -> MM ()
uniRebind r s = do
	instS <- isVarInst s
	-- not 100% sure
	-- TODO check, if s is an inst, but do not rebinds, is it ok?
	-- unless instS $ error $ "uniRebind got not an Inst ref = " ++ show s
	p <- getVarParent s
	tp <- getVarTimeTag p
	tr <- getVarTimeTag r
	when (tr < tp) $ do
		guard instS
		delVarChild p s
		addVarChild r s
		setVarParent s r

uniMerge :: RefType -> RefType -> MM a -> MM a
uniMerge x y k = 
	if x == y then error $ "uniMerge got x x for x = " ++ show x
	else do setVarValue y (Ref x); k

revOrd :: Ordering -> Ordering
revOrd LT = GT
revOrd EQ = EQ
revOrd GT = LT

-- parameter k means continuation :: MM a
uniEq :: Evaluable Type => EqId -> Type -> Type -> MM a -> MM a
uniEq = uniEq' EQ

uniEqReval :: Evaluable Type => Type -> MM Type
uniEqReval (Ref r) = 
	isVarFree r >>= choice (return $ Ref r) (getVarValue r >>= uniEqReval)
uniEqReval (PGet t n) = evalProperty n t >>= uniEqReval
uniEqReval t = return t

uniEq' :: Evaluable Type => Ordering -> EqId 
		-> Type -> Type -> MM a -> MM a
uniEq' o i a b k = do
	a' <- uniEqReval a
	b' <- uniEqReval b
	uniEq'' o i a' b' k

uniEq'' :: Evaluable Type => Ordering -> EqId 
		-> Type -> Type -> MM a -> MM a
uniEq'' _ i a@(App _ _ _) b k = eqEqOk i a b k
uniEq'' _ i a b@(App _ _ _) k = eqEqOk i a b k
uniEq'' EQ i a@(Var _ _ _ _) b k = 
	uniEq' LT i a b $ uniEq' GT i a b k
uniEq'' EQ i a b@(Var _ _ _ _) k = uniEq' EQ i b a k
uniEq'' LT i a@(Var _ _ _ _) b k = do
	(a',j) <- unquantify False a
	(j',w) <- normalize j (uniEq' LT i a' b k)
	(getEq i) >>= (quantify j') >>= (setEq i) -- Int <: Number
	return w
uniEq'' LT i a b@(Var _ _ _ _) k = do
	(b',j) <- unquantify True b
	(j',w) <- normalize j (uniEq' LT i a b' k)
	(getEq i) >>= (quantify j') >>= (setEq i) -- Instantiate <: Skolemize
	return w
uniEq'' GT i a@(Var _ _ _ _) b k = uniEq' LT i b a k
uniEq'' GT i a b@(Var _ _ _ _) k = uniEq' LT i b a k
uniEq'' _ _ (Ref x) (Ref y) k = if x == y then k else do
	skolemX <- isVarSkolem x
	skolemY <- isVarSkolem y
	tx <- getVarTimeTag x
	ty <- getVarTimeTag y
	let s b r t = (if b then " Sk(" else " It(") ++ 
			show r ++ "," ++ show t ++ ")"
	when (skolemX && (tx > ty)) $ fail $ 
		"uniEq " ++ s skolemX x tx ++ s skolemY y ty
	when (skolemY && (ty > tx)) $ fail $ 
		"uniEq " ++ s skolemX x tx ++ s skolemY y ty
	if tx < ty then uniMerge x y k else uniMerge y x k
uniEq'' _ i (Ref x) b k = do
	isVarSkolem x >>= choice
		(fail $ "uniEq Skolem(" ++ show x ++ ") " ++ show b)
		(uniAddTerm i x b k)
uniEq'' o i a b@(Ref _) k = uniEq' (revOrd o) i b a k
uniEq'' o i (PSet t n v) b k = do
	(b',p) <- popProperty n b
	uniEq'' o i t b' $ uniEq'' o i v p k
uniEq'' o i a b@(PSet _ _ _) k = uniEq' (revOrd o) i b a k
uniEq'' _ _ (Cls c) (Cls d) k = 
	if clsEq c d then k 
	else fail $ "uniEq " ++ show c ++ " " ++ show d
uniEq'' o i (Cls c) b k = do
	t <- clsGetSubtype c (Cls c)
	uniEq' o i t b k
uniEq'' o i a b@(Cls _) k = uniEq' (revOrd o) i b a k
uniEq'' o i (Lam s1 a1 r1) (Lam s2 a2 r2) k = 
	if s1 == s2 then uniEq' o i a1 a2 $ uniEq' o i r1 r2 k
	else fail $ "uniEq LamLeft LamRight"
uniEq'' o i (Lam s p1 r1) b k = do
	(p2,r2,v) <- makeLam False s b -- TODO is false here right (it is not!), or should it be like when 'Var' ?
	(v',w) <- normalize v $ uniEq' o i p2 p1 $ uniEq' o i r1 r2 k
	(getEq i) >>= (quantify v') >>= (setEq i)
	return w
uniEq'' o i a b@(Lam _ _ _) k = uniEq' (revOrd o) i b a k
uniEq'' _ _ (PGet _ _) _ _ = error $ "uniEq'' got PGet"
uniEq'' _ _ _ (PGet _ _) _ = error $ "uniEq'' got PGet"
uniEq'' _ i a b k = eqEqOk i a b k -- LCA and GCD

uniLeqReval :: Evaluable Type => ((Type,Type) -> Type) -> Type -> MM Type
uniLeqReval q (Ref z) = do
	instZ <- isVarInst z
	if instZ then return (Ref z) else do
		skolZ <- isVarSkolem z
		(if skolZ then do liftM q $ getVarBounds z else getVarValue z)
		>>= uniLeqReval q
uniLeqReval q (PGet t n) = evalProperty n t >>= uniLeqReval q
uniLeqReval _ t = return t

uniLeq :: Evaluable Type => EqId -> Bool -> Type -> Type -> MM a -> MM a
uniLeq i True a@(Ref x) b@(Ref y) k = if x == y then k else do
	a' <- uniEqReval a -- keep skolems
	b' <- uniEqReval b -- keep skolems
	uniLeq' i True a' b' k
uniLeq i e a@(Ref x) b@(Ref y) k = if x == y then k else do
	a' <- uniLeqReval snd a
	b' <- uniLeqReval fst b
	uniLeq' i e a' b' k
uniLeq i e a b k = do
	a' <- uniLeqReval snd a
	b' <- uniLeqReval fst b
	uniLeq' i e a' b' k

uniLeq' :: Evaluable Type => EqId -> Bool -> Type -> Type -> MM a -> MM a
uniLeq' i True (Ref x) (Ref y) k = uniEq'' LT i (Ref x) (Ref y) k
uniLeq' i True (Ref x) b k = uniAddTerm i x b k
uniLeq' i True a (Ref y) k = uniAddTerm i y a k
uniLeq' i e a@(App _ _ _) b k = eqLeqOk i e a b k
uniLeq' i e a b@(App _ _ _) k = eqLeqOk i e a b k
uniLeq' _ _ (Cls c) _ k | clsIsNothing c = k
uniLeq' _ _ _ (Cls c) k | clsIsThing c = k
uniLeq' i e a@(Ref _) b@(Ref _) k = eqLeqOk i e a b k
uniLeq' i e a@(Ref _) b@(Cls _) k = eqLeqOk i e a b k
uniLeq' i e a@(Cls _) b@(Ref _) k = eqLeqOk i e a b k
uniLeq' _ _   (Cls c)   (Cls d) k = guard (clsLeq c d) >>= (const k)
uniLeq' i e a@(Var _ _ _ _) b k = do -- Int <: Number
	(a',j) <- unquantify False a
	(j',w) <- normalize j (uniLeq i e a' b k)
	(getEq i) >>= (quantify j') >>= (setEq i)
	return w
uniLeq' i e a b@(Var _ _ _ _) k = do -- Instantiate <: Skolemize
	(b',j) <- unquantify True b
	(j',w) <- normalize j (uniLeq i e a b' k)
	(getEq i) >>= (quantify j') >>= (setEq i)
	return w
uniLeq' i e (PSet t n v) b k = do
	(b',p) <- popProperty n b
	uniLeq i e t b' $ uniLeq i e v p k
uniLeq' i e a (PSet t n v) k = do
	(a',p) <- popProperty n a
	uniLeq i e a' t $ uniLeq i e p v k
uniLeq' i e (Lam s1 a1 r1) (Lam s2 a2 r2) k =
	if s1 == s2 then do uniLeq i e a2 a1 $ uniLeq i e r1 r2 k
	else fail $ "uniLeq LamLeft LamRight"
uniLeq' i e a (Lam s p2 r2) k = do
	(p1,r1,v) <- makeLam False s a
	(v',w) <- normalize v $ uniLeq i e p2 p1 $ uniLeq i e r1 r2 k
	(getEq i) >>= (quantify v') >>= (setEq i)
	return w
uniLeq' i e (Lam s p1 r1) b k = do
	(p2,r2,v) <- makeLam True s b
	(v',w) <- normalize v $ uniLeq i e p2 p1 $ uniLeq i e r1 r2 k
	(getEq i) >>= (quantify v') >>= (setEq i)
	return w
uniLeq' _ _ (PGet _ _) _ _ = error $ "uniLeq' got PGet"
uniLeq' _ _ _ (PGet _ _) _ = error $ "uniLeq' got PGet"
uniLeq' i e (Lca a b) c k = uniLeq i e a c $ uniLeq i e b c k
uniLeq' i e c (Gcd a b) k = uniLeq i e c a $ uniLeq i e c b k
uniLeq' i e a b k = eqLeqOk i e a b k

---------------------------------------------
--  optimize bounds
---------------------------------------------

optimizeBoundsK :: Evaluable Type => MM a -> MM a
optimizeBoundsK k = eqLoopK optEq optLeq k

optEq :: Evaluable Type => EqId -> Type -> Type -> MM a -> MM a
optEq i a b k = do
	a' <- uniEqReval a
	b' <- uniEqReval b
	optEq' i a' b' k

optEq' :: Evaluable Type => EqId -> Type -> Type -> MM a -> MM a
optEq' i a b k = 
	optDigLeq i a b $ optDigLeq i b a $ eqEqOk i a b $ k

optLeq :: Evaluable Type => EqId -> Bool -> Type -> Type -> MM a -> MM a
optLeq i e a b k = do
	a' <- uniEqReval a
	b' <- uniEqReval b
	optLeq' i e a' b' k

optLeq' :: Evaluable Type => EqId -> Bool -> Type -> Type -> MM a -> MM a
optLeq' i e a b k = 
	optDigLeq i a b $ eqLeqOk i e a b $ k

optEval :: Evaluable Type => ((Type,Type) -> Type,(Type,Type) -> Type) 
		-> Type -> MM Type
optEval _ t@(Cls _) = return t
optEval (f1,_)   (Ref r) = 
	isVarFree r >>= choice 
		(liftM f1 $ getVarBounds r) 
		(getVarValue r)
optEval f   (Lca a b) = do
	a' <- optEval f a
	b' <- optEval f b
	lca a' b'
optEval f   (Gcd a b) = do
	a' <- optEval f a
	b' <- optEval f b
	gcd a' b'
optEval (f1,f2)   (Lam b a r) = do
	a' <- optEval (f2,f1) a
	r' <- optEval (f1,f2) r
	return (Lam b a' r')
optEval f   (PSet t n v) = do
	t' <- optEval f t
	v' <- optEval f v
	return $ pSet t' n v'
optEval f   (PGet t n) = do
	optEval f t >>= evalProperty n >>= optEval f
optEval f   (App b g x) = do
	g' <- optEval f g
	x' <- optEval f x
	eval (App b g' x') >>= optEval f
optEval (f1,f2) t@(Var _ b _ _) = do
	(t',i) <- unquantify False t
	case i of 
		FInfo [] -> error $ "ensure unexpected FInfo []"
		FInfo [(_,x)] -> setVarValue x (f1 b)
		FInfo _ -> error $ "ensure unexpected FInfo: " ++ show i
	t'' <- optEval (f1,f2) t'
	quantify i t''

optDigLeq :: Evaluable Type => EqId -> Type -> Type -> MM a -> MM a
optDigLeq _ a b k0 = 
	let 
		g (Cls(C 0 0)) _ = True
		g _ (Cls(C 0 0)) = True
		g _ _ = False
	in do
	a' <- optEval (fst,snd) a
	b' <- optEval (snd,fst) b
	-- this is ok
	--   f <= g  <==> f(0) <= g(1)
	optTLeq a' b'
	-- but this is wrong
	-- values of 'no' and 'th' should be reevaluated for each variable separatedly because
	--   f(0,0,...) `fsg` g(1,0,0,...) <= x <= g(1,1,...) `gsf` f(1,0,...)
	-- not 
	--   f(0,0,...) `fsg` g(1,1,...) <= x <= g(1,1,...) `gsf` f(0,0,...)
	-- as it is implemented right now
	-- this 'improper' bounds are implemented for efficiency reasons
	-- since `fsg` and `gsf` are antitone in their second arguments, 
	-- the bounds are a little weaker and all correct solutions will be accepted
	th <- fsg b' a'
	no <- gsf a' b'
	if g no th then k0 else do
		optTLeq no th
		vs <- uniGetVars [a,b] RefSet.empty
		RefSet.fold (f no th) k0 vs where
			f nt ti i k = do
				(no,th) <- getVarBounds i
				optTLeq nt th
				optTLeq no ti
				no' <- lca no nt
				th' <- gcd th ti
				setVarBounds i (no',th')
				k


--------------------------------------
-- LEQ and EQ
--------------------------------------

-- Subtyping relation, less or equal
-- T <: T
-- (forall a. T) <: T[a=U]
-- T <: (forall a. T) if a \notin FV(T) 
-- examples:
--   Int <: Number
--   (forall a.[a]) <: [Int]
--   A <: B if (\x.x :: A -> B)

optTLeq :: Evaluable Type => Type -> Type -> MM ()
optTLeq a@(App _ _ _) b@(App _ _ _) = do
	a' <- optEval (fst,snd) a
	b' <- optEval (snd,fst) b
	optTLeq a' b'
optTLeq a@(App _ _ _) b = do
	a' <- optEval (fst,snd) a
	optTLeq a' b
optTLeq a b@(App _ _ _) = do
	b' <- optEval (snd,fst) b
	optTLeq a b'
optTLeq a@(PGet _ _) b = optEval (fst,snd) a >>= flip optTLeq b
optTLeq a b@(PGet _ _) = optEval (snd,fst) b >>= optTLeq a
optTLeq a@(Var _ _ _ _) b = do
	(t,i) <- unquantify False a
	optTLeq t b
	_ <- quantify i t
	return ()
optTLeq a b@(Var _ _ _ _) = do
	(t,i) <- unquantify True b
	optTLeq a t
	_ <- quantify i t
	return ()
optTLeq (Ref r) b = do
	a <- isVarFree r >>= choice 
		(liftM fst $ getVarBounds r) 
		(getVarValue r)
	optTLeq a b
optTLeq a (Ref r) = do
	b <- isVarFree r >>= choice 
		(liftM snd $ getVarBounds r) 
		(getVarValue r)
	optTLeq a b
optTLeq   (Lam b1 a1 r1)   (Lam b2 a2 r2) = do
	guard $ b1 == b2
	optTLeq a2 a1
	optTLeq r1 r2
optTLeq a@(Lam b1 _ _) b = do
	(a2,r2,i) <- makeLam True b1 b 
	optTLeq a (Lam b1 a2 r2)
	_ <- quantify i (Lam b1 a2 r2)
	return ()
optTLeq a b@(Lam b2 _ _) = do
	(a1,r1,i) <- makeLam False b2 a 
	optTLeq (Lam b2 a1 r1) b
	_ <- quantify i (Lam b2 a1 r1)
	return ()
optTLeq (Lca a b) c = do
	optTLeq a c
	optTLeq b c
optTLeq a b@(Lca _ _) = do
	b' <- optEval (snd,fst) b
	optTLeq a b'
optTLeq c (Gcd a b) = do
	optTLeq c a
	optTLeq c b
optTLeq a@(Gcd _ _) b = do
	a' <- optEval (fst,snd) a
	optTLeq a' b
optTLeq   (PSet t n v) b = do
	(b',p) <- popProperty n b
	optTLeq t b' 
	optTLeq v p
optTLeq a   (PSet t n v) = do
	(a',p) <- popProperty n a
	optTLeq a' t
	optTLeq p v
optTLeq   (Cls ca)   (Cls cb) = guard $ clsLeq ca cb
-- all the matches were done already,
-- so the two following lines are not needed
--optTLeq   (Cls c) b = clsGetSubtype c >>= flip optTLeq b
--optTLeq a   (Cls c) = clsGetSubtype c >>= optTLeq a


-----------------------------------------------
-- IS TRUE, EXISTS, ENSURE
-----------------------------------------------

instance Evaluable Type => Ensurable Formulae where
	ensure TT = return ()
	ensure FF = fail $ "ensure got FF"
	ensure (Leq _ a b) = do
		a' <- enEval (snd,fst) a -- (snd,fst) are only for skolems
		b' <- enEval (fst,snd) b
		optTLeq a' b' -- here are no vares, so trivial optTLeq is just enough
	ensure (Eq a b) = do ensure (Leq True a b) ; ensure (Leq True b a)
	ensure (And []) = return ()
	ensure (And (x:xs)) = do ensure x; ensure (And xs)
	ensure f@(Qua False _ _ _ _) = do
		(f',i) <- unquantify False f
		case i of 
			FInfo [] -> error $ "ensure unexpected FInfo []"
			FInfo [(_,x)] -> getVarFormulae x >>= ensure
			FInfo _ -> error $ "ensure unexpected FInfo: " ++ show i
		ensure f'
		_ <- quantify i TT
		return ()
	ensure   (Qua True x b f1 f2) = do
		ctx <- getCtx
		let ls = whereTrue ctx x b f1
		forM_ ls $ \c -> do
			(f',i) <- unquantify False (Qua True x b (Eq (Ref x) c) f2)
			(i',()) <- normalize i $ ensure f'
			_ <- quantify i' TT
			return ()

-- TODO merge eval, optEval, enEval and any other eval
enEval :: Evaluable Type => ((Type,Type) -> Type,(Type,Type) -> Type) -> Type -> MM Type
enEval _ t@(Cls _) = return t
enEval (f1,_)   (Ref r) = do
	free <- isVarFree r
	when free $ do 
		(a,b) <- getVarBounds r
		isVarSkolem r >>= choice 
			(setVarValue r $ f1 (a,b))
			(mplus (setVarValue r a) (setVarValue r b))
	getVarValue r
enEval f   (Lca a b) = do
	a' <- enEval f a
	b' <- enEval f b
	lca a' b'
enEval f   (Gcd a b) = do
	a' <- enEval f a
	b' <- enEval f b
	gcd a' b'
enEval (f1,f2)   (Lam b a r) = do
	a' <- enEval (f2,f1) a
	r' <- enEval (f1,f2) r
	return (Lam b a' r')
enEval f   (App b g x) = do
	g' <- enEval f g
	x' <- enEval f x
	eval (App b g' x') >>= enEval f
enEval f   (PSet t n v) = do
	t' <- enEval f t
	v' <- enEval f v
	return $ pSet t' n v'
enEval f   (PGet t n) = enEval f t >>= evalProperty n >>= enEval f
enEval (f1,f2) t@(Var _ b _ _) = do
	(t',i) <- unquantify False t
	case i of 
		FInfo [] -> error $ "ensure unexpected FInfo []"
		FInfo [(_,x)] -> setVarValue x (f1 b)
		FInfo _ -> error $ "ensure unexpected FInfo: " ++ show i
	t'' <- enEval (f1,f2) t'
	quantify i t''

whereTrue :: Evaluable Type => Context -> RefType -> (Type,Type) -> Formulae -> [Type]
whereTrue ctx x (a,b) f1 = 
	List.filter (\y -> not $ null $ runMM (m y) ctx) [a,b] where -- TODO
	m t = do 
		(f',i) <- unquantify False (Qua True x (typeNothing,typeThing) (Eq (Ref x) t) f1)
		(i',()) <- normalize i $ ensure f'
		_ <- quantify i' TT
		return ()

-- a stub for further extensions
exists :: Context -> Type -> Bool
exists c t = True

